[Zantema - RTA'97, Example 5]

Example 5 in [Zantema - RTA'97]

Summary: Ex5_Zan97

CS-TRS format
OBJ format
Negative results:
1. Lucas' transformation (Extra variables)
2. CSRPO
Positive results:

CS-TRS Ex5_Zan97 (file Ex5_Zan97.csr)

Functions:  f if c true false

Constructors:  c true false

Variables:  X Y

Arities: 

ar(f) = 1
ar(if) = 3
ar(c) = 0
ar(true) = 0
ar(false) = 0

Replacement map: 

µ(f)={1}
µ(if)={1,2}
µ(c)={}
µ(true)={}
µ(false)={}

Rules:  (file Ex5_Zan97)

f(X) -> if(X,c,f(true))
if(true,X,Y) -> X
if(false,X,Y) -> Y

The CS-TRS in OBJ format (file Ex5_Zan97.obj):

obj Ex5_Zan97 is
  sort S .
  op f : S -> S .
  op if : S S S -> S [strat (1 2 0)] .
  op c : -> S .
  op true : -> S .
  op false : -> S .
  vars X Y : S .
  eq f(X) = if(X,c,f(true)) .
  eq if(true,X,Y) = X .
  eq if(false,X,Y) = Y .
endo

Negative results

The µ-termination of Ex5_Zan97 cannot be proved by using Lucas' transformation. The TRS Ex5_Zan97_L:
```
    f(X) -> if(X,c)
    if(true,X) -> X
    if(false,X) -> Y
    
```
contains extra variables.

The mu-termination of R can be proved by using CSRPO (counterexample due to Albert Rubio):

    m(if,3)=f

    f > if,f',true

    for first rule, but then 

    f(X) > if(X,c,f'(true))   f> if

    if(false,X,Y_f) > Y       if > f  !

    fails since f > if

Positive results

Ex5_Zan97 is proved µ-terminating in [Zan97, Example 5] by using Zantema's transformation. The TRS Ex5_Zan97_Z:

    f(X) -> if(X,c,n__f(true))
    if(true,X,Y) -> X
    if(false,X,Y) -> activate(Y)
    f(X) -> n__f(X)
    activate(n__f(X)) -> f(X)
    activate(X) -> X

can be proved terminating (use MuTerm).

The µ-termination of Ex5_Zan97 can also be proved by using Ferreira and Ribeiro's transformation. The the TRS Ex5_Zan97_FR:

    f(X) -> if(X,c,n__f(n__true))
    if(true,X,Y) -> X
    if(false,X,Y) -> activate(Y)
    f(X) -> n__f(X)
    true -> n__true
    activate(n__f(X)) -> f(activate(X))
    activate(n__true) -> true
    activate(X) -> X

is terminating (use MuTerm).

The µ-termination of Ex5_Zan97 can also be proved by using Giesl and Middeldorp's transformation: the TRS Ex5_Zan97_GM:

    a__f(X) -> a__if(mark(X),c,f(true))
    a__if(true,X,Y) -> mark(X)
    a__if(false,X,Y) -> mark(Y)
    mark(f(X)) -> a__f(mark(X))
    mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3)
    mark(c) -> c
    mark(true) -> true
    mark(false) -> false
    a__f(X) -> f(X)
    a__if(X1,X2,X3) -> if(X1,X2,X3)

is terminating (use MuTerm).

The µ-termination of Ex5_Zan97 is proved in [Luc04, Example 11] by using a polynomial interpretation (computed with MuTerm):

   Proof of termination for CS-TRS  Ex5_Zan97:

   [f](X) = 3.X + 2
   [if](X1,X2,X3) = X1.X3 + X1 + X2 + 1
   [c] = 0
   [true] = 0
   [false] = 1

The µ-termination of Ex4_Zan97 can also be proved by using CSDP (computed with MuTerm).